es:event_system{i:l}, e':es-E(es). e:es-E(es). ((es-first(es; e))  es-le(es; e; e')) 

latex

Definitions	x:A. B(x), x:A. B(x), P  Q, t  T, prop{i:l}, P  Q, x. t(x), es-le(es; e; e'), P  Q, guard(T), A c B, wellfounded{i:l}(A; x,y.R(x;y)), x(s), decidable(P), trans(T; x,y.E(x;y))
Lemmas	es-locl-wellfnd, es-E wf, assert wf, es-first wf, es-le wf, es-locl wf, event system wf, decidable assert, es-pred wf, es-pred-locl, es-le-trans